$\forall$$R$:es\_realizer\{i:l\}, $i$:Id, $k$:Knd. ($\uparrow$write{-}restricted($R$; $i$; $k$)) $\Rightarrow$ ($\uparrow$R{-}has{-}loc($R$; $i$))